ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da), es:event_system{i:l}, i:Id.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). (loc(e) = i)  subtype_rel(es-valtype(es; e); ma-valtype(da; es-kind(es; e))))
 (ecl-es-halt(es; x)  {e:es-E(es)| loc(e) = i} {e2:es-E(es)| loc(e2) = i} prop{i:l}) 

latex

Definitions

subtype(S; T), x,y,z. t(x;y;z), x,y,z,w. t(x;y;z;w), A  B, ff, guard(T), sq_type(T), x. t(x), tt, x,y. t(x;y), A, P  Q, P  Q, False, A c B, if b then t else f fi , ecl-es-halt(es; x), prop{i:l}, , t  T, P  Q, x:A. B(x), x(s), P  Q, Unit, x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2), ,

Lemmas

l member wf, alle-between2 wf, alle-between1 wf, le int wf, l-all wf, existse-between2 wf, nat plus wf, nat plus inc, ecl-ex wf, Knd wf, fpf wf, ecl wf, event system wf, top wf, id-deq wf, fpf-cap wf, es-kind wf, es-valtype wf, Id wf, es-E wf, l exists wf, es-pstar-q wf, eq int wf, ifthenelse wf, es-loc-pred, es-pred wf, es-first wf, existse-between3 wf, ma-valtype wf, decl-state wf, le wf, false wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, Knd sq, es-val wf, es-vartype wf, es-state-subtype, es-state-when wf, es-first-since wf, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool wf, es-loc wf, nat wf, ecl ind wf